$\forall$$T$:Type, $L$:$T$ List, $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel-$1}}$, $a$, $b$:$T$.
\\[0ex]$a$ before $b$ $\in$ swap($L$;$i$;$i$+1) $\Rightarrow$ $a$ before $b$ $\in$ $L$ $\vee$ $a$ $=$ $L$[$i$+1] \& $b$ $=$ $L$[$i$]